With the increasing complexity and shorter development cycles of current digital systems, it has become more difficult to verify that circuits designed for these systems have the correct structure and functionality. To assist in reducing errors and streamlining the development process, formal equivalence verification techniques are used to verify that circuit descriptions preceding and following a design step define the same functionality. Currently, the predominant formal equivalence verification technique is combinational verification, in which input and output logic cones of state elements (elements which store values) are compared between a model specification circuit, and a new implementation circuit. This technique generally involves building binary decisions diagrams (BDDs) to plot the various states that a state element may enter as a function of the inputs it is provided. If a BDD constructed for a state element X in the specification circuit is equivalent to a BDD constructed for element X′ of the implementation circuit, then it is concluded that the circuits have identical functionality with respect to the particular state element. To complete the verification process, BDDs are constructed and compared for each state element of the specification circuit.
The combinational formal verification process requires that analogous state elements are compared between the specification and implementation circuits. However, the process of building BDDs is very difficult because state element mappings are often unknown. In practice, there is no automatic correspondence between state elements of the two circuits because, for example, not all the state elements retain their unique identifiers or “names” from step to step in the design process. In fact, often more than fifty percent of the state elements in a circuit are not name-mapped. Therefore, prior to formal verification, a state element mapping must be constructed which maps, or draws an inter-circuit correspondence between, state elements of the specification and implementation circuits.
The theoretical purpose of state mapping is to produce a one-to-one correspondence between state elements of the specification and implementation circuits. In practice, however, one-to-many and inverse mappings often occur in addtion to one-to-one mappings. One-to-many mappings exist when the implementation circuit contains duplicate versions of a single state element found in the specification circuit. In inverse mappings (as opposed to direct mappings), state elements in the two circuits are structurally equivalent but exactly opposite in function, so that, for example, a set of equivalent logic conditions that produce a value bit-stream of ‘110’ in a given state element A will produce a value bit-stream of ‘001’ in inverted mapped element A′. While it is especially crucial to identify such inverted mapped state elements which have equivalent but opposite output, it is also important to identify “don't care” input conditions for which mapped state elements are permitted to have different outputs. Without prior identification of such don't care conditions, such mappings can be invalidated during functional simulations. Both inverse mappings and don't cares must accordingly be accounted for during the state element mapping process.
As of the present time, attempts at automatic state mapping have been largely unsuccessful, in part because they have not appropriately accounted for the variety of state element contingencies described. Moreover, manual state mapping currently requires as much as several days per functional circuit block. What is needed, therefore, is an optimized automatic state mapping process that properly utilizes available information concerning state element input conditions, appropriately accounts for inverse mappings and provides a dramatic improvement in efficiency over manual state mapping techniques.